00100	GIVEAX(SI1,SCWORLD W0);
00200	
00300	GIVEAX(SI2,I0 ε BASIS W0);
00400	
00500	GIVEAX(SI3,(∀ X)(X ε TERMS(TORD I0,W0)
00600		⊃ SUCC X ε TERMS(TORD I0,W0)
00700		∧ (∀ S)(S ε STATES W0 ⊃
00800		C(SUCC X,S) = SUCC C(X,S))));
00900	
01000	GIVEAX(SI4,(∀ X)(X ε TERMS(TORD I0,W0)
01100		⊃ PRED X ε TERMS(TORD I0,W0)
01200		∧ (∀ S)(S ε STATES W0 ⊃
01300		C(PRED X,S) = PRED C(X,S))));
01400	
01500	GIVEAX(SI5,(∀ X)(∀ Y)(X ε TERMS(TORD I0,W0)
01600		∧ Y ε TERMS(TORD I0,W0)
01700			⊃
01800		INTEQ(X,Y) ε TERMS(TORD TV,W0)
01900		∧ (∀ S)(S ε STATES W0 ⊃
02000		C(INTEQ(X,Y),S) = INTEQ(C(X,S),C(Y,S)))));
     

00900	END;